; <lemma>
;  <title>ch910_ring.2</title>
;  <origin>ch910_ring | ring_lln_1 | INITIALISATION/inv2/INV</origin>
(benchmark ch910_ring_2
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="f" type="INTEGER"/>
;  </typenv>
  :extrafuns ((f Int))
;  m : max({f})
  :extrafuns ((m Int))
  :extramacros (
                 ; {f}
		 (enum1 (lambda (?i Int) . (= ?i f)))
		 (Nat (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 )
;  max({f})
  :assumption (forall (?i Int) (implies (in ?i enum1)
				 (<= ?i m)))
  :assumption (in m enum1)
; <goal>f = max({f})</goal>
  :formula
  (not
      (= f m)
    )
)
; </lemma>

